(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](cs, ncs, node, colorednodes, Cons(x, xs), colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Rewrite Strategy: INNERMOST

(1) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
colorednoderest[Ite][True][Ite][True][Let]/0
colorednoderest[Ite][True][Ite][True][Let]/1
colorednoderest[Ite][True][Ite][True][Let]/2
colorednoderest[Ite][True][Ite][True][Let]/3
colorednoderest[Ite][True][Ite][True][Let]/4

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

colorof(node, Cons(CN(cl, N(name, adjs)), xs)) → colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) → and(False, eqColorList(cs1, cs2))
eqColorList(Cons(Red, cs1), Cons(Red, cs2)) → and(True, eqColorList(cs1, cs2))
eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) → and(False, eqColorList(cs1, cs2))
revapp(Cons(x, xs), rest) → revapp(xs, Cons(x, rest))
revapp(Nil, rest) → rest
possible(color, Cons(x, xs), colorednodes) → possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
possible(color, Nil, colorednodes) → True
colorrest(cs, ncs, colorednodes, Cons(x, xs)) → colorednoderest(cs, ncs, x, colorednodes, Cons(x, xs))
colorrest(cs, ncs, colorednodes, Nil) → colorednodes
colorof(node, Nil) → NoColor
colornode(Cons(x, xs), N(n, ns), colorednodes) → colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
colornode(Nil, node, colorednodes) → NotPossible
colorednoderest(cs, Cons(x, xs), N(n, ns), colorednodes, rest) → colorednoderest[Ite][True][Ite](possible(x, ns, colorednodes), cs, Cons(x, xs), N(n, ns), colorednodes, rest)
colorednoderest(cs, Nil, node, colorednodes, rest) → Nil
graphcolour(Cons(x, xs), cs) → reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
eqColorList(Cons(c1, cs1), Nil) → False
eqColorList(Nil, Cons(c2, cs2)) → False
eqColorList(Nil, Nil) → True
eqColor(Yellow, NoColor) → False
eqColor(Yellow, Yellow) → True
eqColor(Yellow, Blue) → False
eqColor(Yellow, Red) → False
eqColor(Blue, NoColor) → False
eqColor(Blue, Yellow) → False
eqColor(Blue, Blue) → True
eqColor(Blue, Red) → False
eqColor(Red, NoColor) → False
eqColor(Red, Yellow) → False
eqColor(Red, Blue) → False
eqColor(Red, Red) → True
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
getNodeName(N(name, adjs)) → name
getNodeFromCN(CN(cl, n)) → n
getColorListFromCN(CN(cl, n)) → cl
getAdjs(N(n, ns)) → ns
eqColor(NoColor, b) → False
reverse(xs) → revapp(xs, Nil)
colorrestthetrick(cs1, cs, ncs, colorednodes, rest) → colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)

The (relative) TRS S consists of the following rules:

and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) → x
possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) → possible(color, xs, colorednodes)
colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) → colorrestthetrick(xs, cs, ncs, colorednodes, rest)
colorof[Ite][True][Ite](False, node, Cons(x, xs)) → colorof(node, xs)
colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) → colornode(xs, node, colorednodes)
colorednoderest[Ite][True][Ite](False, cs, Cons(x, xs), node, colorednodes, rest) → colorednoderest(cs, xs, node, colorednodes, rest)
colorednoderest[Ite][True][Ite](True, cs, ncs, node, colorednodes, Cons(x, xs)) → colorednoderest[Ite][True][Ite][True][Let](colorrest(cs, cs, Cons(CN(ncs, node), colorednodes), xs))
possible[Ite][True][Ite](True, color, adjs, colorednodes) → False
colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) → colorrest(cs, ncs, colorednodes, rest)
colornode[Ite][True][Ite](True, cs, node, colorednodes) → CN(cs, node)

Rewrite Strategy: INNERMOST

(3) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
colorof(S(y96_3), Cons(CN(cl, N(0, adjs)), xs)) →+ colorof(S(y96_3), xs)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(CN(cl, N(0, adjs)), xs)].
The result substitution is [ ].

(4) BOUNDS(n^1, INF)